IO/@

First true pure free IO monad as inductive type in Erlang:

> 'IO':
'Monad'/0      '[>>=]'/0      getLine/0     pure/0         putLine/0

> rp(term_to_binary('IO':'Monad'())).
<<131,112,0,0,0,67,1,44,109,229,18,14,54,134,74,22,94,63,
  98,214,172,215,124,0,0,0,2,0,0,0,0,100,0,2,73,79,97,2,
  98,1,99,111,40,103,100,0,13,110,111,110,111,100,101,64,
  110,111,104,111,115,116,0,0,1,22,0,0,0,0,0>>

$ cat Monad

λ(a : *) → λ(cmd : #Cmd/@ #IO/@ a) → cmd (#IO/@ a) (λ(b : *) → #IO/[>>=] b a)
(#IO/pure a)

$ cat IO/[>>=]

λ(a : *) → λ(b : *) → λ(m : ∀(IO : *) → ∀(GetLine_ : (#String/@ → IO) → IO) →
∀(PutLine_ : #String/@ → IO → IO) → ∀(Pure_ : a → IO) → IO) → λ(f : a → ∀(IO :
*) → ∀(GetLine_ : (#String/@ → IO) → IO) → ∀(PutLine_ : #String/@ → IO → IO) →
∀(Pure_ : b → IO) → IO) → m (∀(IO : *) → ∀(GetLine_ : (#String/@ → IO) → IO) →
∀(PutLine_ : #String/@ → IO → IO) → ∀(Pure_ : b → IO) → IO) (λ(_x : #String/@ →
∀(IO : *) → ∀(GetLine_ : (#String/@ → IO) → IO) → ∀(PutLine_ : #String/@ → IO →
IO) → ∀(Pure_ : b → IO) → IO) → λ(IO : *) → λ(GetLine_ : (#String/@ → IO) → IO)
→ λ(PutLine_ : #String/@ → IO → IO) → λ(Pure_ : b → IO) → GetLine_ (λ(_x :
#String/@ ) → _x@1 _x IO GetLine_ PutLine_ Pure_)) (λ(_x : #String/@ ) → λ(_x :
∀(IO : *) → ∀(GetLine_ : (#String/@ → IO) → IO) → ∀(PutLine_ : #String/@ → IO →
IO) → ∀(Pure_ : b → IO) → IO) → λ(IO : *) → λ(GetLine_ : (#String/@ → IO) → IO)
→ λ(PutLine_ : #String/@ → IO → IO) → λ(Pure_ : b → IO) → PutLine_ _x@1 (_x IO
GetLine_ PutLine_ Pure_)) (λ(r : a) → f r (∀(IO : *) → ∀(GetLine_ : (#String/@
→ IO) → IO) → ∀(PutLine_ : #String/@ → IO → IO) → ∀(Pure_ : b → IO) → IO) (λ(_x
: #String/@ → ∀(IO : *) → ∀(GetLine_ : (#String/@ → IO) → IO) → ∀(PutLine_ :
#String/@ → IO → IO) → ∀(Pure_ : b → IO) → IO) → λ(IO : *) → λ(GetLine_ :
(#String/@ → IO) → IO) → λ(PutLine_ : #String/@ → IO → IO) → λ(Pure_ : b → IO)
→ GetLine_ (λ(_x : #String/@ ) → _x@1 _x IO GetLine_ PutLine_ Pure_)) (λ(_x :
#String/@ ) → λ(_x : ∀(IO : *) → ∀(GetLine_ : (#String/@ → IO) → IO) →
∀(PutLine_ : #String/@ → IO → IO) → ∀(Pure_ : b → IO) → IO) → λ(IO : *) →
λ(GetLine_ : (#String/@ → IO) → IO) → λ(PutLine_ : #String/@ → IO → IO) →
λ(Pure_ : b → IO) → PutLine_ _x@1 (_x IO GetLine_ PutLine_ Pure_)) (λ(_x : b) →
λ(IO : *) → λ(GetLine_ : (#String/@ → IO) → IO) → λ(PutLine_ : #String/@ → IO →
IO) → λ(Pure_ : b → IO) → Pure_ _x))

$ cat IO/@

λ (a : *)
→ ∀ (IO : *)
→ ∀ (GetLine_ : (#String/@ → IO) → IO)
→ ∀ (PutLine_ : #String/@ → IO → IO)
→ ∀ (Pure_ : a → IO) → IO

$ om print type a "#IO/Monad"
( ∀ (a: *1)
→ ( ∀ (cmd: ( ∀ (Cmd: *1)
  → ( ∀ (Bind: ( ∀ (b: *1)
    → ( ∀ (_: ( ∀ (IO: *1)
      → ( ∀ (GetLine_: ( ∀ (_: ( ∀ (_: ( ∀ (S: *1)
            → ( ∀ (N: S)
            → ( ∀ (C: ( ∀ (_: S)
              → S))
            → ( ∀ (C: ( ∀ (_: S)
              → S))
            → S)))))
          → IO))
        → IO))
      → ( ∀ (PutLine_: ( ∀ (_: ( ∀ (S: *1)
          → ( ∀ (N: S)
          → ( ∀ (C: ( ∀ (_: S)
            → S))
          → ( ∀ (C: ( ∀ (_: S)
            → S))
          → S)))))
        → ( ∀ (_: IO)
        → IO)))
      → ( ∀ (Pure_: ( ∀ (_: b)
        → IO))
      → IO)))))
    → ( ∀ (_: ( ∀ (_: b)
      → Cmd))
    → Cmd))))
  → ( ∀ (Pure: ( ∀ (r: a)
    → Cmd))
  → Cmd))))
→ ( ∀ (IO: *1)
→ ( ∀ (GetLine_: ( ∀ (_: ( ∀ (_: ( ∀ (S: *1)
      → ( ∀ (N: S)
      → ( ∀ (C: ( ∀ (_: S)
        → S))
      → ( ∀ (C: ( ∀ (_: S)
        → S))
      → S)))))
    → IO))
  → IO))
→ ( ∀ (PutLine_: ( ∀ (_: ( ∀ (S: *1)
    → ( ∀ (N: S)
    → ( ∀ (C: ( ∀ (_: S)
      → S))
    → ( ∀ (C: ( ∀ (_: S)
      → S))
    → S)))))
  → ( ∀ (_: IO)
  → IO)))
→ ( ∀ (Pure_: ( ∀ (_: a)
  → IO))
→ IO))))))
ok

$ om print fst erase a "#IO/Monad"
( λ cmd
→ ((cmd ( λ m
→ ( λ f
→ (((m ( λ _x
→ ( λ GetLine_
→ ( λ PutLine_
→ ( λ Pure_
→ (GetLine_ ( λ _x
→ ((((_x@1 _x) GetLine_) PutLine_) Pure_)))))))) ( λ _x
→ ( λ _x
→ ( λ GetLine_
→ ( λ PutLine_
→ ( λ Pure_
→ ((PutLine_ _x@1) (((_x GetLine_) PutLine_) Pure_)))))))) ( λ r
→ ((((f r) ( λ _x
→ ( λ GetLine_
→ ( λ PutLine_
→ ( λ Pure_
→ (GetLine_ ( λ _x
→ ((((_x@1 _x) GetLine_) PutLine_) Pure_)))))))) ( λ _x
→ ( λ _x
→ ( λ GetLine_
→ ( λ PutLine_
→ ( λ Pure_
→ ((PutLine_ _x@1) (((_x GetLine_) PutLine_) Pure_)))))))) ( λ _x
→ ( λ GetLine_
→ ( λ PutLine_
→ ( λ Pure_
→ (Pure_ _x))))))))))) ( λ _x
→ ( λ GetLine_
→ ( λ PutLine_
→ ( λ Pure_
→ (Pure_ _x)))))))
ok